package ch.epfl.lara.matcheck.verify.transform;

import ch.epfl.lara.matcheck.ast._

object ExtractorBody2Formula extends AbstractConversion2Formula {

  def apply(expr: Expr): (Formula,String) = {
    generated_names = Nil
    Convert(expr)
  }
    
  
  private object Convert {
    
    implicit def packres(e: E): (Formula,String) = pack(e)
    
    implicit def string2elem(s: String): Element = Element(s)
    
    
    private def pack(e: E): (Formula,String) = {
      val fresh = freshName(e.makeName)
      (Eq(fresh,e),fresh)
    }
    
    def apply(expr: Option[Expr]): (Formula,String) = expr match {
      case None => Tru
      case Some(expr) => this(expr)
    }
    
    def apply(body: Expr): (Formula,String) = body match {
      case Call(ObjectId(name),_,_) if name.getName == Constants.SOME => 
        Tru
      case Ident(name) if name.getName == Constants.NONE => 
        Flse
        
      case If(cond,then,elze) =>
        val (condition,res_if) = this(cond)
        val(then_cond,res_then) = this(then)
        val(elze_cond,res_elze) = this(elze)
        val res = freshName("if")
        val eq = Equality(res,And(Imply(res_if,res_then),Imply(Neg(res_if),res_elze)))      
        (And(And(condition,And(then_cond,elze_cond)),eq),res)
       
      case Match(scrutinee,tpe,cases) =>
        val (lhs_scrut,res_scrut) = this(scrutinee)
        val scrut_tpe = Equality(freshName("scrutinee"),In(res_scrut,TreeExpr2Formula(tpe)))
        val scrutinee_axiom = And(lhs_scrut,scrut_tpe)
        var left = scrutinee_axiom
        var cases_res: List[Formula] = Nil
       
        for(CaseDef(_,pattern,guard,body)<-cases) {
        
          val Imply(p_lhs,p_rhs) = Pattern2Formula(res_scrut,pattern)
          append_names(Pattern2Formula.generated_fresh_names)
          
          val (guard_lhs,guard_res) = this(guard)
          
          val (body_lhs,body_res) = this(body)
        
          val fresh = freshName("case")
          val case2formula = And(And(p_rhs,guard_res),
                                 And(body_res,
                                     cases_res.foldLeft[Formula](Tru)((l,r) => And(l,Neg(r)))))
        
          left = And(And(And(left,p_lhs),And(guard_lhs,body_lhs)),Equality(fresh,case2formula))
                                             
          cases_res = fresh :: cases_res
        }
      

        val result = freshName("pm")
        var pm: Formula = Tru
        if(cases_res.length == 0) () 
        else if(cases_res.length == 1) pm = cases_res.head
        else for(i<-List.range(0,cases_res.length-1);j<-List.range(i+1,cases_res.length)) {
          pm = And(pm,Neg(And(cases_res(i),cases_res(j))))  
        }
      
        val pm_res = Equality(result,
                            And(pm,
                            cases_res.foldLeft[Formula](Flse)((l,r) => Or(l,r))))
                             
        (And(left,pm_res),result)
        
        
      case e: Expr => 
        val res = TreeExpr2Formula(e)
        append_names(TreeExpr2Formula.generated_fresh_names)
        res
    }
  }
}
